COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.sec(Lambda Calculus)
C00010 00003	.ss(Deductive system,,R12:)
C00017 00004	%73. %1and%7 4.%1##We list the axioms and rules of inference for the ∪λ∩-calculus
C00022 00005	
C00028 ENDMK
C⊗;
.sec(Lambda Calculus)
.ss(Introduction)
.begin indent 15,15;
Wadsworth's analysis of Scott's λ-calculus model provides a good illustration
of the dangers of confusing computation with deduction.  In his thesis he
studies various properties of β-reduction with the aim of showing that "what
we would expect and hope for computationally" is indeed true in the model.  One
such hope was that because of "the close analogy between programs which terminate
and well-formed expressions with normal forms", well-formed expressions which have
normal forms should be distinguishable semantically from those which don't.
Unfortunately this turns out not to be the case in D%4∞%1.  Initially this
fact caused Wadsworth to reject D%4∞%1 as an adequate model.  However later on
he realized that having a normal form - a notion based on the λ-conversion
INFERENCE rules - shouldn't be crudely equated with the COMPUTATIONAL notion
of non-termination.  In fact his stuff on head normal forms is a (successful)
attempt to distinguish computational and deductive aspects of β-conversion,
i.e., to separate those conversions which are computations from those which arn't.
.end
.begin nofill;
					M. J. C. Gordon
.end

.BEGIN "LOCALAT"
.at "πf"⊂"%3f%1"⊃


.at "πg"⊂"%3g%1"⊃

.at "π0"⊂"%30%1"⊃
.at "π1"⊂"%31%1"⊃
.at "π2"⊂"%32%1"⊃
.at "π3"⊂"%33%1"⊃
.at "π5"⊂"%35%1"⊃
.at "π7"⊂"%37%1"⊃
.at "π8"⊂"%38%1"⊃
.at "π9"⊂"%39%1"⊃

.at "πy"⊂"%3y%1"⊃

.at "πx"⊂"%3x%1"⊃

.at "πz"⊂"%3z%1"⊃

The starting point for the λ-calculus is a notation for function-denoting
expressions.  In mathematics, when we want to denote a function we usually
introduce a new letter along with a function definition.  For example,
to denote the function which squares a number and adds π1 to it we might
write: πf, where πf(πx)=πx%82%1+π1.

The λ-calculus offers a way to denote functions anonymously, so that we need
not give a name to each function we wish to use and the definition is clear
from the notation.  Using the λ-notation, the above function would be
denoted %3λx.x%82%1+π1, which can be read as: that function which for argument
πx has value πx%82%1+π1.

Such λ-expressions may then occur wherever function-denoting symbols may 
occur.  Thus,
.begin center;
(1)   (%3λx.x%82%1+π1)(π2)
.end
makes sense wherever πf(π2) does.  To evaluate πf(π2), we need to look up
the definition of πf, then apply it to the argument π2.  To evaluate the
expression (1), we substitute the argument π2 for the %3⊗→bound variable↔←%1
πx throughout the %3⊗→body↔←%1 πx%82%1+π1 so that
.begin center;
(%3λx.x%82%1+π1)(π2) = π2%82%1+π1 = %35%1
.end
This operation of substituting the argument in the body is known as ⊗→β-reduction↔←.
A second operation applicable to λ-expressions is the systematic change of bound
variables.  Just as we regard πf, where πf(πx)=πx%82%1+π1 and πf, where
πf(πy)=πy%82%1+π1 as denoting the same function, the λ-expressions 
%3λx.x%82%1+π1 and %3λy.y%82%1+π1 are regarded as equivalent.  The conversion
occurring between these two expressions is an example of ⊗→α-conversion↔←.

For simplicity of syntax the λ-calculus allows only functions of one 
argument.  A multi-argument function is treated as a function of its first
argument which yields a function of its remaining arguments.

.BEGIN INDENT 10,10;
		For example:  πf, where πf(πx, πy)#=#πx+πy
	could be thought of as πf, where πf(πx)#=#πg%4x%1 and
				   where πg%4x%1(πy)#=#πx+πy
		or, in λ-notation:
			%3λx.(λy.x+y)%1
.END

This technique for multi-argument functions is known as "⊗→Sch⊗onfinkeling↔←" (since
the device was originally suggested by Sch⊗onfinkel, although some people call
it "Currying" since the notation was popularized by Curry).
In the above example it is shown that a function may have a function as value;
a function might also take a function as argument.
.begin indent 10,10;
for example, %3twice%1 is a function which given a function πg as argument, 
returns the composition of πg with itself as value.  Thus %3twice%1 is denoted
by %3λg.(λy.g(g(y)))
.end

When the λ-calculus is set up as a formal system, we extend the informal usage
in two ways:
.begin indent 10,10;
a)  No type restrictions are placed on the formation of function applications.  For
any two expressions %dM%1 and %dN%1, the application %dM(N)%1 is well-formed.  Thus
all expressions of the system may be regarded both as functions and as arguments
to functions.

b)  We deal with the pure λ-calculus, which does not include symbols for
constants (such as numbers or addition), that is, we allow only functions
definable by means of the λ-operation alone.
.end
.END "LOCALAT"
.ss(Deductive system,,R12:)
%71.%1 A countable set of symbols:
.BEGIN NOFILL;indent 10,10;
identifiers (variables) %da, b, c, ..., x, y, z, ...%1
predicate symbol: %d=%1
auxiliary symbols: %dλ, ., (, )%1
.end
We use "≡" for syntactic identity.

.group
.begin tabit1 (10);nofill;

%72.%1 The set of terms, %Dλ%1-terms, or well-formed expressions (wfes) is defined as follows:
\<term> ::= <identifier> | %d(%1<term><term>%d)%1 | %d(λ%1<identifier> %d.%1<term>%d)%1
\<identifier> ::= %da%1 | %db%1 ...| %dx%1 | %dy%1 ...

.end
.apart
.begin fill indent 1,3;
1. Every identifier is a term.

2. If ?M and ?N are terms, then the %3⊗→combination↔←%1 ∪(M N)∩ is a term, the parts ?M
and ?N being called its %3⊗→rator↔←%1 and %3⊗→rand↔←%1, respectively. Note that
we are now representing function application by juxtaposition of terms, i.e.,
∪(M N)∩; we might occasionally revert to the usual notation when no
confusion is likely.

3. If ?x is an identifier and ?M is a term, then the %3⊗→abstraction↔←%1 ∪(λx.M)∩
is a term, the parts ?x and ?M being called its %3⊗→bv↔←%1 (for bound variable) and %3⊗→body↔←%1,
respectively.
.end

The formulae of the %Dλ%1-calculus consist of equations between terms.
.begin center;

<wff> ::= <term> = <term>
.end
If ?M and ?N are terms, then ∪M=N∩ is a well-formed formula.
Parentheses may be omitted from %Dλ%1-terms according to the following conventions:
.begin indent 0,5;
1) Association to the left: ?M0?M1 ... ?Mn%1 
stands for ∪((#...#((?M0?M1)?M2)#...#)?Mn)∩.

2) The scope of the "∪.∩" in abstractions extends as far to the right 
as possible; i.e., to the first unmatched "∪)∩" or to the end of the term; whichever
occurs first.

3) Consecutive ∪λ∩'s may be collapsed to a single ∪λ∩, for example,
 ∪λ?x0N∪.#M∩ stands for
∪(λ?x0∪.(λ?x1∪#.(...#(λ?xn∪#.#M)#...#)))∩.

.end
An occurrence of a variable ?x in a term ?M is %3⊗→bound↔←%1 if it is 
inside some part of ?M of the form ∪λx.#M'∩; all other occurrences of ?x
in ?M are %3⊗→free↔←%*. We shall write ⊗→%dFV(M)%1↔← and ⊗→%dBV(M)%1↔← for the sets of
variables occurring free and bound, respectively, in ?M.
Note that the same variable may occur both free and bound in a term: 
.BEGIN INDENT 10,10;

for
example, in ∪λy.x(λx.xy)∩, the leftmost occurrence of %dx%1 is free while the
others are bound.
.END

The definition of substitution requires some care to prevent unwanted capture of 
free variables. We write ⊗→%d[N/x]M%1↔← for the %3⊗→substitution↔← of ?N for the 
free occurrences of ?x %3in ?M. The tricky case is when ?N contains free variables
which are bound in ?M (case 3c, below).  An inductive definition of substitution is:
.begin indent 10,10;
.nofill;
.begin indent 10,15;
1. If ?M is an identifier ?y
   a) if ∪y≡x∩, then ∪[N/x]y = N∩
   b) if ∪y≥x∩, then ∪[N/x]y = y∩
.end
2. If ?M is a combination ?M0?M1, then ∪[N/x](∩?M0?M1∪) = ([N/x]?M0∪)([N/x]∩?M1%d)%1.

.begin indent 10,15;group
3. If ?M is an abstraction ∪(λy.∩?M0%d)%1,
   a) if ∪x≡y∩, or if ∪x≤FV(?M0∪)∩, then ∪[N/x](λy.?M0∪) = λy.?M0∩

   b) if ∪y≤FV(N)∩, then  ∪[N/x](λy.?M0∪) = λy.[N/x]?M0

   c) otherwise, ∪xεFV(?M0∪), yεFV(N), x≥y∩, thus ∪[N/x](λy.?M0∪) = λw.[N/x]([w/y]?M0∪)∩ 
.end
.fill;
.indent 15,15;
 where ∪w∩ is the first (or any other we wish to specify) identifier in the 
alphabetical list of identifiers, which does not occur free in ∪N∩ or ?M0.
.end
%73. %1and%7 4.%1##We list the axioms and rules of inference for the ∪λ∩-calculus
together.
.begin nofill; indent 15,15;

1. = is an equivalence relation
   (%gr%1) ∪M=M∩ for all terms ∪M∩
   (%gt%1) from ∪M=N∩ and ∪N=L∩, infer ∪M=L∩
   (%gs%1) from ∪M=N∩, infer ∪N=M∩

2. = is substitutive
   (%gm%1) from ∪N=N'∩, infer ∪MN=MN'∩
   (%gn%1) from ∪M=M'∩, infer ∪MN=M'N∩
   (%gx%1) from ∪M=N∩, infer ∪λx.M=λx.N∩

3. ⊗→conversion rules↔←
   (∪α∩) ∪λx.M=λy.[y/x]M∩, provided ∪y≤FV(M)
   (β) (λx.M)N=[N/x]M
   (?h∪) λx.Mx=M  ∩provided ∪x≤FV(M)∩

This system is called the ⊗→%glbh%1-calculus↔←.

.end
The rules (?α) and (?β) are obvious formalizations of the operations of
?α- and ?β-conversion mentioned earlier.  The rule (?h) is equivalent to the rule
of functional extensionality. 
.begin center;

(Ext)  from ∪Mx=Nx∩ for ∪x≤FV(M), x≤FV(N)∩ infer ∪M=N∩
.end
 For, notice that, if ∪x≤FV(M)∩ then ∪(λx.Mx)N=MN∩, for all terms ?N, by
?β-conversion, i.e., the terms ∪λx.Mx∩ and ?M are functionally equivalent, they
yield the same thing when applied to any argument.

The concept of a %3context%1 is the opposite of a subterm.  A %3⊗→context↔←%1, ⊗→%dC%1[ ]↔←,
consists of all of a term except for one subterm.  We use empty brackets [ ] to
indicate the missing subterm. 
.begin center;

 For example, ∪C[ ] ≡ λx.x([ ]a)∩
.end
The result of filling the missing subterm in ?C[ ] with a term ?M is denoted
∪C[M]∩.  For any other term ?N, ∪C[N]∩ denotes the same term as ∪C[M]∩ except
that the indicated occurrence of ?M is replaced by ?N.  For the example above,
we have ∪C[yx] ≡ λx.x(yxa)∩.  Contexts are useful for stating results which
hold for all terms.

We "evaluate" ?λ-terms by eliminating abstractions as far as possible, which
means replacing terms of the form on the left of the rules (?β) and (?h) by
the terms on the right.  This is captured in the concepts of reduction and
normal form.

A term of the form ∪R ≡ (λx.M)N∩ is called a ?β-%3⊗→redex↔←%1 and ∪R' ≡ [N/x]M∩
is called its %3⊗→contractum↔←%1.  If ?X is a term containing a ?β-redex ?R, i.e.,
∪X ≡ C[R]∩ for some context ∪C[ ]∩, the operation of replacing ?R by ?R'
to yield ∪X'≡C[R']∩ is called a ?β-%3⊗→contraction↔←%1; in the other direction,
the replacement of ?R' by ?R is called a ?β-%3⊗→abstraction↔←%1.  A sequence of
(possibly 0) ?β-contractions is called a ?β-%3⊗→reduction↔←%1, written
∪X#β-$r#∪X'∩.

A term of the form ∪P≡(λx.Mx)∩ is called an ?h-%3redex%1 if ∪x≤FV(M)∩, and then,
?M is called its %3contractum%1.  The definitions of ?h-%3contraction, ?h-%3abstraction,
∪X ?h-$r ∪X'∩, etc., follow by analogy with those of ?β.

When it is of no interest which reduction rules are being applied we simply
write ⊗→%dX#%3red%d#X'%1↔←.  Change of bound variables (?α-conversion) is, of course,
symmetric, and we shall trivially allow ?α-conversion in a reduction sequence.

It is easily verified that the relation $r is reflexive, transitive, and substitutive, but
not symmetric.  (Neither, in general, is it anti-symmetric.)

We say that ?M is %3⊗→convertible↔←%1 to ?N, written ⊗→%dM#%3cnv#%dN%1↔←, if their equality can be
proved from the deductive system given above, that is, if ∪M=N∩ is a theorem
of the ∪λβ∩?h-calculus.⊗↓To be precise we should be referring throughout to the
∪λβ∩?h-calculus, since it is possible to treat the subject without including
the rule (?h).  However, since we will always be referring to the above formal
system, no confusion should arise from the terminology ?λ-calculus.←
If ∪M=N∩ can be proved using only the conversion rule (?β) we may write
∪M#β-$c#?N; similarly for ?α-$c or ?h-$c.  We will usually perform conversions
between terms informally and not bother with the formal proof of their equality.
.begin indent 10,10; nofill;
For example, informally
.begin center;
∪x((λy.yx)(λz.z)) $c ∪x((λz.z)x) $c ∪xx∩
.end
formally, the proof would look like
.begin tabit2 (15,55);
\1. ∪(λy.yx)(λz.z) = [(λz.z)/y](yx)∩\by (?β)
\################∪= (λz.z)x∩\def. of substitution
\2. ∪(λz.z)x = [x/z]z = x∩\by (?β) and substitution
\3. ∪(λy.yx)(λz.z) = x∩\by (%gt%1) from 1,2
\4. ∪x((λy.yx)(λz.z)) = xx∩\by (%gm%1) from 3.
.end
.end

A %3closed%1 term is one which contains no free variables; after Curry, ⊗→closed terms↔←
are also sometimes called ⊗→combinators↔←.  We are primarily interested in the
properties of closed terms, however we often need to prove more general results
about terms with free variables, in particular, when we wish to use inductive
arguments based on the structure of terms (since even a closed term may have
subterms containing free variables).

In the case of closed terms, we are often interested in their behaviour as
functions.  For instance, a closed term ?M is ∪I%3-solvable%1 if it can be
applied as a function (generally, of several arguments) to yield the identity
function
.begin center;
∪I ≡ λx.x
.end
More precisely, ?M is ⊗→%dI%1-solvable↔← if there exist terms ?A0k (k≥0) such that

.begin center;
(2)  ?M?A0K#$c#∪I∩
.end
If ?M has free variables, we say it is ∪I∩-solvable if there exists a substitution
of closed terms for the free variables such that the resulting closed term is
∪I∩-solvable.
.begin indent 10,10,10;
A term ?M with free variables ?x0n is said to be ∪I∩-%3solvable%1 if there
exist terms ?N0n and terms ?A0k such that
.begin center;

(3)  ([?N0n/?x0n]?M)?A0K $c ∪I∩
.end
where ⊗→[%dN%40%1, ..., %dN%4n%1/%dx%40%1, ..., %dx%4n%1]↔← denotes the 
⊗→multiple substitution↔← defined in the obvious
way from the single case ∪[N/x]∩, assuming ?x0n are distinct variables.
.end

Using contexts, (2) and (3) may be stated in the form ∪C[M] $c ∪I∩, for
some context ?C[ ].  The appropriate contexts, respectively, are
.begin center;

(2')  ∪[ ]?A0K

(3')  ∪(λ?x0N∪.[ ])?N0N?A0K
.end

.R18:
Both of these contexts are examples of what we call a %3⊗→head context↔←%1, that
is they are of the form
.begin center;

∪(λ?x1N∪.[ ])?X1M n≥0, m≥0
.end
for variables ?x1n, and terms ?X1m.  Thus, for %7any%1 term ?M (closed or not),
?M is ?I-%3solvable%1 if there is a head context ∪C[ ]∩ such that
∪C[M]#$c#∪I∩.